Nuprl Lemma : l_before_member2
11,40
postcript
pdf
T
:Type,
L
:(
T
List),
a
,
b
:
T
. l_before(
a
;
b
;
L
;
T
)
(
a
L
)
latex
Definitions
t
T
,
l_before(
x
;
y
;
l
;
T
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
P
Q
,
P
Q
,
P
Q
,
True
,
P
Q
,
prop{i:l}
Lemmas
sublist
wf
,
member
iff
sublist
,
sublist
transitivity
,
cons
sublist
cons
,
nil
sublist
,
and
functionality
wrt
iff
,
or
functionality
wrt
iff
,
true
wf
origin